es:ES, A:Type, l:IdLnk, tg:Id, ds:x:Id fp Type,
conds:k:Knd fp V:Type  (State(ds)V(A + Top)).
(k:Knd. (k  dom(conds))  (hasloc(k;source(l))))
 (e:E. (kind(e) = rcv(l,tg)  Knd)  (valtype(e) r A))
 (e:E.
 (loc(e) = source(l)  Id)
  (kind(e)  dom(conds))
  ((valtype(e) r (conds(kind(e)).1)) & (state@loc(e) r State(ds))))
 (p:(e:E.
 (p:(Dec((isrcv(e))
 (p:(& lnk(e) = l
 (p:(& loc(sender(e)) = source(l)  Id
 (p:(& (kind(sender(e))  dom(conds)))).
 (k:Knd.
 (k  dom(conds))
  k(v:conds(k).1) sends on l [tg:A, p.let s,v = p in (conds(k).2)(s,v) <state, v>]?[])
  glues(es;
  glues(A;
  glues((e.sender(e));
  glues((e.outl((conds(kind(e)).2)((state when e),val(e))));
  glues(es-triggers(es;source(l);ds;conds);
  glues((es-in-port(es;l;tg)|p))) 

latex

Definitions

x:A. B(x), IdLnk, a:A fp B(a), P  Q, P & Q, t  T, , x. t(x), A c B, T, True, x(s), glues(es; B; g; f; Ia; Ib), g glues Ia:Qa f Ib:Rb, Q = f== P, {I}, Q ==f== P, x:A. B(x), False, can-apply(f;x), f is Q-R-pre-preserving on P, Top, S  T, Inj(A;B;f), es-in-port(es;l;tg), X(e), do-apply(f;x), if b then t else f fi , tt, ff, b, isl(x), outl(x), SqStable(P), P  Q, k(v:B) sends on l [tg:T, f <state, v>]?[], Dec(P), P  Q, A, P  Q, {T}, E(X), , Unit,

Lemmas

Knd wf, assert wf, fpf-dom wf, Kind-deq wf, fpf-trivial-subtype-top, decl-state wf, top wf, conditional-send-p wf, pi1 wf, fpf-ap wf, pi2 wf, decidable wf, es-lnk wf, es-loc wf, es-sender wf, es-kind wf, Id wf, lsrc wf, es-state wf, es-E wf, rcv wf, es-valtype wf, hasloc wf, l member wf, event system wf, es-is-interface wf, es-interface-restrict wf, es-in-port wf, sq stable from decidable, es-isrcv wf, decidable assert, es-is-interface-restrict, es-sender-causl, es-causle weakening, es-triggers wf, es-is-interface-triggers, member-fpf-domain, isl wf, es-state-when wf, es-state-subtype, es-vartype wf, es-val wf, es-is-interface-in-port, es-kind-rcv, fpf-domain wf, es-le wf, es-is-interface-restrict2, sender-le-pre-preserving, can-apply wf, es-E-interface wf, es-interface-val-restrict, outl wf, es-state-subtype-iff, eq knd wf, bool wf, assert-eq-knd, bnot wf, not wf, not functionality wrt iff, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, true wf, false wf, es-rcv-kind